This is a trial PR in preparation for a PR upstream @jmid @kayceesrk @stedolan @anmolsahoo25

Thanks for the PR. I'll ask a few initial questions

1. Is there a performance cost on code that is not compiled with --enable-tsan?
   • Does the compilation take longer or more memory?
   • Does the compiled program run longer?
   • Is there a code size impact for the compiled program?
   • Does the compiled program use more memory?
2. I assume that, unlike C/C++, given that OCaml has some mutability information, instrumentation can be avoided on many accesses. Is this exploited? If so, I am surprised to see that the performance impact is on the same range as tsan instrumentation on C/C++. What am I missing?
3. On a cursory look, the change looks fairly invasive. It adds 2640 lines and deletes 100 lines. There are 105 files changed. Can you comment on these changes? For example, how many of the 2640 lines and 105 files changed is new tests, for example?
4. Lots of the CI runs are failing. Why?

ThreadSanitizer supports inserts calls to the ThreadSanitizer runtime library, which tracks accesses to shared data and reports races.

support

Perhaps @sadiqj may also want to take a look as he has a good sense of runtime and instrumentation.

1. Is there a performance cost on code that is not compiled with --enable-tsan?

• Does the compilation take longer or more memory?
• Does the compiled program run longer?
• Is there a code size impact for the compiled program?
• Does the compiled program use more memory?

There should be no added cost without --enable-tsan.

• The compilation process should not change except for a few if Config.tsan tests on non-critical paths.
• The generated code is the same.
• There should be no size impact for executables statically linked with the runtime, as all of our changes are guarded by an #ifdef WITH_THREAD_SANITIZER directive.
• The memory usage of the compiled program should be the same.

2. I assume that, unlike C/C++, given that OCaml has some mutability information, instrumentation can be avoided on many accesses. Is this exploited?

Yes, from OCaml code, we instrument only the accesses to mutable locations. On the other hand, the C runtime is also instrumented, and C instrumentation has no mutability information, so the instrumentation there is likely to be more costly.

If so, I am surprised to see that the performance impact is on the same range as tsan instrumentation on C/C++. What am I missing?

The memory usage is better than C/C++/Go: ours seems to be 2x-7x, whereas https://www.youtube.com/watch?v=5erqWdlhQLA reports 5x-10x. But the slowdown can indeed be seen as disappointing. I have three hypotheses:

• the instrumented C runtime may suffer a bigger slowdown and drag down the performance of the program;
• exception and effect handling is much more costly than in non-instrumented OCaml as we have to unwind the stack every time, even with raise_notrace;
• maybe we are still instrumenting too many OCaml accesses due to incomplete mutability information; e.g. I recently substantially improved performance by no longer instrumenting header reads. It would require some work to look into improvement opportunities. It would also be interesting to investigate pathological cases such as the skiplist test mentioned above.

3. On a cursory look, the change looks fairly invasive. It adds 2640 lines and deletes 100 lines. There are 105 files changed. Can you comment on these changes? For example, how many of the 2640 lines and 105 files changed is new tests, for example?

Yes: the changes to the test suite only totalize 1583 insertions and 35 deletions on 45 files. So they constitute the bulk of the diff. The rest is split evenly between asmcomp/ and runtime/, where it is organized as described in the first message. The changes to the runtime are conditioned to the WITH_THREAD_SANITIZER constant. There are also a few non-invasive changes to the makefiles.

Finally, in the runtime, a portion of the diff (~100 lines) is due to this comment repeated several times:

+CAMLno_tsan /* FIXME Race reports from this function clog the tests of user
+               programs, so we disable instrumentation here. However, Further
+               investigation would be needed about the cause of these race
+               reports.
+               */
 static int try_update_object_header(value v, volatile value *p, value result,
                                     mlsize_t infix_offset) {

(As a side note, we had to silence many TSan reports internal to the runtime, which we intend to report separately.)

the instrumented C runtime may suffer a bigger slowdown and drag down the performance of the program;

regarding this, a promising track of improvement is to un-instrument all C functions that do not perform any synchronization operations critical for TSan.

Investigating the CI failures now.

Thanks. It would be useful to incorporate some of the answers to my questions into the PR message.

Thank you for taking the time to look at this @kayceesrk. I updated the PR message with the new elements.

The CI failures were due to me forgetting to push an updated configure.

Thanks for the trial PR! I think the PR text is well-written and gives a good intro with relevant background info.
I took a look at the diff last night, and spotted a few things. I'm not experienced in the run-time system so take the below with a grain of salt:

• In the emitters: failwith "not implemented" seems a bit short. A non-suspecting user hitting this will not necessarily know what isn't implemented.
• Perhaps you could add a high-level explanation of what C/Ireturn_addr is used/needed for?
• I spotted a few needless changes that might as well be omitted to keep the diff minimal (I suspect they are a result of repeated rebasing):
  • the Makefile has an unrelated newline change in the clean target
  • runtime/caml/stack.h has an unrelated comment inserted

The other thing that you should include is how TSAN instrumentation is used to detect data race under the Multicore OCaml primitives i.e, translation of OCaml memory model to C memory model. This came up in the discussion at https://discuss.ocaml.org/t/ann-threadsanitizer-support-for-ocaml-5-0-0-first-public-release/10975. It would be useful to add a section on how the translation works.

Given the last open question from Guillaume, do you think we're at a stage where we are sure that the technical work has been completed and there are no open questions? If there are open questions, mention them explicitly in the PR message.

@jmid Thank you for your comments, I will follow the suggestions.

Given the last open question from Guillaume, do you think we're at a stage where we are sure that the technical work has been completed and there are no open questions? If there are open questions, mention them explicitly in the PR message.

Guillaume has pinpointed something that I overlooked. I completed the instrumentation of memory accesses when I was not aware of the subtleties of translating the OCaml memory model to C, and I did not go back to question this instrumentation later.

As a result, the current mapping from OCaml operations to C11 operations, that is used to inform TSan, does not quite reflect the correct mapping (ocaml/ocaml#10995):

In bold are the operations for which the mapping from OCaml to C11 memory operations is not faithful to the one described in ocaml/ocaml#10995.

In addition, Guillaume’s question is relevant and we did not lay it out clearly before: are we mapping OCaml memory operations to well-defined C programs (but at the risk that TSan does not report OCaml data races), or mapping OCaml memory operations to possibly buggy C programs (when there is an OCaml data race)?

I do not think any of this is a huge blocker, but the technical question should indeed be answered, and the implementation possibly corrected. I am leaning in favor of mapping OCaml data races to buggy C programs, but I need to verify that race-free programs will then always be mapped to race-free C programs.

I edited to fix some wrong lines in the table.

or mapping OCaml memory operations to possibly buggy C programs (when there is an OCaml data race)?

Isn't this what we want? So that the race detector can tell us when things go wrong? Does that lead to more false positives?

More generally, can you comment on the soundness of TSAN for C++ programs and our encoding of TSAN for OCaml programs? A sound race detector has no false positives. If the underlying system is unsound, then there is no point in going for soundness with our encoding. Of course, reducing false positives is a worthwhile effort.

Yes, I think that mapping racy OCaml operations to buggy C programs is what we want.

can you comment on the soundness of TSAN for C++ programs and our encoding of TSAN for OCaml programs?

TSan is claimed to have no false positives (there are no papers describing TSan’s current algorithm, but see this slide: https://youtu.be/5erqWdlhQLA?t=1975), except sometimes when “there is tiny probability to miss a data race” (https://github.com/google/sanitizers/wiki/ThreadSanitizerAlgorithm#state-machine).

Does that lead to more false positives?

I think it might, or at least I cannot find a good mapping right now. We could just take the correct mapping (i.e., not the one above) and turn the operation for non-atomic loads into a plain write; that would ensure that a conflicting read & write to the same non-atomic location are turned into a C11 data race, and I think we don’t lose any happens-before edges that way; but then two conflicting writes do not translate to a data race.

If we signal non-atomic stores as just plain writes, then I think we lose some happens-before edges, which can lead to false positives.

It would be useful to have the input of someone more expert than me in memory models on this question.

I think I can chime in here.

What is ThreadSanitizer doing?

The objective of the ThreadSanitizer instrumentation of OCaml programs is to detect a race. A race is defined if there exist two memory events to a non-atomic location, with at least one being a write. A race exists if there is no happens-before (hb) edge between these two events. The ThreadSanitizer runtime mechanism builds up the hb-relation dynamically and signals if two events satisfying the above condition exist.

Why embed an OCaml program in a C program?

We use the C11 primitives provided by the ThreadSanitizer library to signal the hb-edges between OCaml memory events. For this, we use the existing hb-edges defined between RC11 events. For example, a e1: __tsan_atomic_write(x, release) and e2: __tsan_atomic_read(x, acquire) sets up an hb-edge, provided e2 reads from e1. This is a primitive hb-edge defined in RC11 and happens to coincide with what we need for OCaml as well.

But, since the OCaml memory model has additional hb-edges than RC11, we have to add more synchronization.

Mapping OCaml memory events to C11 primitives

The correct encoding of OCaml memory events to RC11 memory events is as follows. According to the OCaml Memory Model paper, there are 3 conditions for hb -

1. E1 hb E2 whenever E1 is an initial write and E2 is not.
2. E1 hb E2 whenever E1 po E2.
3. E1 hb E2 whenever E1 and E2 access the same atomic location
   3.1. E1 co E2
   3.2. E1 rf E2.

The current mapping is incorrect for the below reasons -

1. The seq_cst ordering on atomic writes create a total order on all writes. But in the OCaml memory model, there is only an hb-order between writes to the same location
2. The semantics of seq_cst in RC11 are broken (refer to Repairing Sequential Consistency in C/C++11)
3. Non-atomic store may acquire from an atomic store (via the fence) which is not required by the OCaml memory model

@kayceesrk
Just to quickly answer question. We are sending OCaml programs defined under the OCaml Memory Model to C programs defined under the RC11 memory model with additional synchronization. As ThreadSanitizer is sound, if there are any races in the C program, there has to be a race in the OCaml program. Thus the procedure is sound since we are only adding hb-edges to the C11 program, we only eliminate potential races (which are not considered races in the OMM model) and do not create new ones. The procedure is complete, since every race under the OCaml memory model will be a race in the C11 + additional synchronization model. This is because adding hb-edges to the C program recreates exactly the hb-relation defined by the OCaml memory model, thus every race in the OCaml model will continue to be a race in the C model.

Thank you for helping with this.

1. The seq_cst ordering on atomic writes create a total order on all writes. But in the OCaml memory model, there is only an hb-order between writes to the same location

I am surprised by this. Does you mean that @stedolan’s mapping at ocaml/ocaml#10995 is wrong?

Sorry I edited the previous mapping. I hope that does not seem confusing.

Thank you for helping with this.

1. The seq_cst ordering on atomic writes create a total order on all writes. But in the OCaml memory model, there is only an hb-order between writes to the same location

I am surprised by this. Does you mean that @stedolan’s mapping at ocaml/ocaml#10995 is wrong?

No, no. I'm wrong there sorry. seq_cst only creates the total coherence order. hb-order may be different from the coherence order. My bad. But the point still stands that, without knowing how ThreadSanitizer induces hb-edges for seq_cst memory events, we may be going too strong and missing out on races that may otherwise be captured.

Edit: I am just trying to remember where C11 is broken when you mix seq_cst and ra accesses. Which is why I suggested the alternative mapping. Will let you know once I get around.

There is a bug in the PLDI 2018 paper.

E1 hb E2 whenever E1 is an initial write and E2 is not.

hb is too strong here and not needed. This came up in the review of the memory model chapter: ocaml/ocaml#11280 (comment). CC @stedolan.

For non-atomic stores, it would be useful to sub-classify them as I have done in ocaml/ocaml#11418 (comment)

we need to discriminate between the following:

1. Initialising writes
2. non-initialising (non-atomic) writes of integers, where no publication of new objects can take place
3. non-initialising (non-atomic) writes of pointers, with possible publication (caml_modify)
4. writes to non-word-sized fields

Please write down the compilation strategy for each of these separately. It will be much clearer this way.

I am surprised by this. Does you mean that @stedolan’s mapping at ocaml/ocaml#10995 is wrong?

Atomic accesses should use seq_cst.

Overall, I think we need to have a correctness argument for compiling OCaml loads to plain loads. Here's my attempt at the soundness theorem

Assuming TSAN analysis for C programs is sound (no false positives), the compilation of OCaml accesses to TSAN instrumentation introduces no false positives.

What do you think? Does the current implementation have this property?

Thank you.

Slight digression, but it would be very useful to have a document that reflects the current state of the knowledge about the memory model. At least for unexperienced readers like me, it’s difficult to find all the information and keep it in mind. As you mention, the PLDI18 paper requires some errata, and there things it doesn’t cover, like the mapping with the C11 model, or other architectures, that are only covered in Github discussions.

I also have an increasing number of bookmarks of Github discussions that explain a particular point (like the publication safety of initializing writes at ocaml/ocaml#10995 (comment)) or explain the need to add a fence (ocaml/ocaml#10972 (comment)) or discuss potential issues (ocaml/ocaml#10992).

Assuming TSAN analysis for C programs is sound (no false positives), the compilation of OCaml accesses to TSAN instrumentation introduces no false positives.

What do you think? Does the current implementation have this property?

I think the current implementation probably doesn’t have it because e.g. OCaml atomic loads are signaled to TSan as acquired loads. I’m hoping that it can be easily fixed to have it by fixing the mapping, though.

Memory model is likely to remain a complex topic given the nature of it. It may be useful to write an extended version of the PLDI 18 paper. The right time to write the paper would be when we have a few more native backends (s390x and power) and we’ve had lockfree data structures used for real. It is possible that the compilation strategy may evolve or new primitive operations may added.

To summarize, here is the current candidate mapping:

I have some more questions.

The optimized mapping in ocaml/ocaml#10995 assumes that you can transform

val = atomic_load_explicit(..., memory_order_acquire);

into:

val = atomic_load_explicit(..., memory_order_relaxed);
atomic_thread_fence(memory_order_acquire);

Does TSAN now understand atomic_thread_fence? See https://gcc.gnu.org/bugzilla/show_bug.cgi?id=97868.

There is also __tsan_atomic_thread_fence: https://github.com/llvm-mirror/compiler-rt/blob/69445f095c22aac2388f939bedebf224a6efcdaf/include/sanitizer/tsan_interface_atomic.h#L214. Not sure what this does.

In the rest of the discussion, I'm assuming that __tsan_atomic_thread_fence actually does what the name indicates.

In OCaml, initialising writes are plenty. But these writes are not visible to other threads unless the newly allocated object is published. So we can optimise initialising writes by pushing the fence after that write to where the publication of the new object can happen. With that here is what I think the mappings will be:

Atomic load

__tsan_atomic_thread_fence(memory_order_acquire);
__tsan_atomic_load(x, memory_order_seq_cst);

See caml_atomic_load: https://github.com/ocaml/ocaml/blob/trunk/runtime/memory.c#L257-L258

Atomic store

__tsan_atomic_thread_fence(memory_order_acquire);
__tsan_atomic_exchange(x, memory_order_seq_cst);
__tsan_atomic_thread_fence(memory_order_release); /* for publication safety */

See caml_atomic_exchange: https://github.com/ocaml/ocaml/blob/trunk/runtime/memory.c#L272-L274

Non-atomic load

__tsan_read(x)

Non-atomic store (initialising)

__tsan_write(x)

Non-atomic store (assignment, integer)

__tsan_atomic_thread_fence(memory_order_acquire);
__tsan_write(x);

Non-atomic store (assignment, pointer)

__tsan_atomic_thread_fence(memory_order_acquire);
__tsan_write(x);
__tsan_atomic_thread_fence(memory_order_release); /* for publication safety */

See caml_modify: https://github.com/ocaml/ocaml/blob/trunk/runtime/memory.c#L154-L156

Non-atomic store (non-word-sized field)

No guarantees are provided for these accesses by the OCaml memory model. Hence, compiling them to

__tsan_writeN(x), where N is one of 8, 16, 32, 64

should be ok as happens-before will have to be established for them by other means (mutex, atomic variables, etc).

What do you think about the proposal above?

Does TSAN now understand atomic_thread_fence? See https://gcc.gnu.org/bugzilla/show_bug.cgi?id=97868.

Still not. A maintainer confirmed to me that it can be simulated using fake atomic accesses.

There is also __tsan_atomic_thread_fence: https://github.com/llvm-mirror/compiler-rt/blob/69445f095c22aac2388f939bedebf224a6efcdaf/include/sanitizer/tsan_interface_atomic.h#L214. Not sure what this does.

Looking at the implementation, it is a dummy function that does nothing regarding TSan’s knowledge of the HB relationships.

In OCaml, initialising writes are plenty. But these writes are not visible to other threads unless the newly allocated object is published. So we can optimise initialising writes by pushing the fence after that write to where the publication of the new object can happen.

Publication safety seems to also be established by address depedencies by some reports (reference ocaml/ocaml#10995 (comment)). I don’t know by what means TSan could take those into account.

What do you think about the proposal above?

Thank you for the updated proposal. I do not think that I, personally, can have a firm opinion about the absence of false positives with this mapping as of now. It certainly looks reasonable, but to completely convince myself that the theorem holds, I would first need to review all the relations needed in the OCaml memory model and verify that they are exactly the relations established by TSan with this mapping. This will take me a bit of work as, as I previously expressed, a lot of the arguments are currently flying over my head, and the information is scattered.

As discussed collectively, rebased on ocaml/ocaml#12108 which allowed a much needed cleaning of the build system aspects of TSan support.

Closing this PR now that the actual PR ocaml/ocaml#12114 has been opened.